Обозначения:
    A - Для любого
    E - существует

Алгоритм: сортировка вставками - ищется максимальный элемент и ставится в конец, потом обрабатывается массив без последнего элемента, ...

Задание: Используя логику Хоара, доказать тотальную корректность программы, сортирующей непустой масив целых числе s[0: n-1] по неубыванию

// ============================================================================
Вход: непустой массив целых чисел s[0: n-1]

i <= n-1;
while i > 0 do
    k <= i; j <= i - 1;

    while j >= 0 do
        if s[j] > s[k] then
            k <= j
        fi;
        j <= j - 1
    od;
    y <= s[k]; s[k] <= s[i]; s[i] <= y;
    i <= i - 1;
od

Выход: s[0: n-1] - массив отсортированный по неубыванию
// ============================================================================
Input: n > 0 && s = s0 - запомним исходный массив для написания условия output

i <= n-1;
while i > 0 do
    k <= i; j <= i - 1;

    while j >= 0 do
        if s[j] > s[k] then
            k <= j
        fi;
        j <= j - 1
    od;
    y <= s[k]; s[k] <= s[i]; s[i] <= y;
    i <= i - 1;
od

Output: n > 0 && A i (0 < i <= n-1 -->  s[i] >= s[i-1]) && // Проверка, что на выходе упорядоченный массив
    && OO

    где OO - это предикат:
    A x ( (E i s[i] = x) --> (* ограничения на i, т.к. непонятно, что происходит за границами массива *)
        A a (
            E j1, j2 ..., ja ( A m, n ( 1 <= m, n <= a && m != n --> jm != jn) --> (* вместо импликации в конце строки должна быть конъюнкция *)
                A m ( 1 <= m <= a --> s0[jm] = x ) )
            -->
            E j1, j2 ..., ja ( A m, n ( 1 <= m, n <= a && m != n --> jm != jn) --> (* та же ошибка *)
                A m ( 1 <= m <= a --> s[jm] = x ) )
            )
        )
    
    // фиксируем, что у нас в руках всё тот же массив (с тем же количеством тех же элементов)
    // Вообще - можно было и проще, но как-то сегодня звёзды у меня не сложились
// ============================================================================
Input: n > 0 && s = s0 && i = n-1

while i > 0 do
    k <= i; j <= i - 1;

    while j >= 0 do
        if s[j] > s[k] then
            k <= j
        fi;
        j <= j - 1
    od;
    y <= s[k]; s[k] <= s[i]; s[i] <= y;
    i <= i - 1;
od

Output: n > 0 && A i (0 < i <= n-1 -->  s[i] >= s[i-1]) && OO
// ============================================================================
Input: n > 0 && s = s0 && i = n-1

env1 = n > 0 && s = s0 && core_env1 && OO
core_env1 = A d ( max(i, 0) < d <= n-1 --> A j, k ( 0 <= j <= d <= k <= n-1 --> s[j] <= s[k]))
// Фактически я требую, чтобы для любого d > i все элементы левее были меньше всех элементов правее

while i > 0 do
    k <= i; j <= i - 1;

    while j >= 0 do
        if s[j] > s[k] then
            k <= j
        fi;
        j <= j - 1
    od;
    y <= s[k]; s[k] <= s[i]; s[i] <= y;
    i <= i - 1;
od

Output: n > 0 && A i (0 < i <= n-1 -->  s[i-1] <= s[i]) && OO

Действительно:
    Input --> env1
    верно, т.к. OO верно (ибо пока ещё s совпадает с s0) и т.к. core_env1 тоже верно, т.к. i = n-1 --> d не существует (т.е. для них для всех - true) 

    env1 && not (i > 0) --> output
    верно, т.к. i <= 0 --> d любое от 0 до n-1 и для каждого из них выполнено
        A j, k ( 0 <= j <= d <= k <= n-1 --> s[j] <= s[k])
    в частности выполнено для k = d и j = d-1, а это и есть требование output (просто посимвольная подстановка)

    Дальше будем доказывать, что

    env1 && (i > 0) {program} env1

// ============================================================================
Input: n > 0 && s = s0 && core_env1 && OO && i > 0
core_env1 = A d ( max(i, 0) < d <= n-1 --> A j, k ( 0 <= j <= d <= k <= n-1 --> s[j] <= s[k]))

k <= i; j <= i - 1;

while j >= 0 do
    if s[j] > s[k] then
        k <= j
    fi;
    j <= j - 1
od;
y <= s[k]; s[k] <= s[i]; s[i] <= y;
i <= i - 1;

Output: n > 0 && s = s0 && core_env1 && OO
// ============================================================================ МЕТКА 1
Я переименую k из алгоритма на u, а то будут коллизии

Input: n > 0 && s = s0 && core_env1 && OO && i > 0 && u = i && j = i-1
core_env1 = A d ( max(i, 0) < d <= n-1 --> A j, k ( 0 <= j <= d <= k <= n-1 --> s[j] <= s[k]))

env2 = n > 0 && s = s0 && core_env1 && OO && i > 0 && u = i && j = i-1 && core_env2
core_env2 = A m (max(0, j+1) <= m <= i-1 --> s[m] <= s[u])
// Фактически, я просто требую, чтобы u указывало на максимальный элемент массива из диапазона s[j: i-1] (т.е. из того диапазона, который мы уже успели пробежать c помощью j)

while j >= 0 do
    if s[j] > s[u] then
        u <= j
    fi;
    j <= j - 1
od;
y <= s[u]; s[u] <= s[i]; s[i] <= y;
i <= i - 1;

Output: n > 0 && s = s0 && core_env1 && OO

Действительно инвариант подходит:
    input --> env
    верно, т.к. всё совпадает, кроме core_env2, но и core_env2 верен, т.к. j = i-1 --> m = i-1, в то время как u = i, но согласно core_env1 для d = i, j = i-1, k = i, s[j] <= s[k] --> s[i-1] <= s[i] --> s[m] <= s[u]

    while_output = env2 && not (j >= 0) -->
         n > 0 && s = s0 && core_env1 && OO && i > 0 && A m (0 <= m <= i-1 --> s[m] <= s[u])
    верно, т.к. not j >= 0 --> j < 0 --> max(0, j+1) = 0

    env2 && (j >= 0) {program} env2
    верно, т.к. мы это докажем дальше, непосредственно следующими шагами (МЕТКА 3)

Вообще после того, как мы пройдём цикл и на выходе получим while_output нам ещё нужно доказать оставшиеся 2 строчки программы, их доказательство продолжится после "МЕТКА 2", а сейчас мы прервёмся на доказательство внутренности цикла
// ============================================================================ МЕТКА 3
Input = n > 0 && s = s0 && core_env1 && OO && i > 0 && core_env2 && j >= 0
core_env2 = A m (max(0, j+1) <= m <= i-1 --> s[m] <= s[u])

if s[j] > s[u] then
    u <= j
fi;
j <= j - 1

Output = n > 0 && s = s0 && core_env1 && OO && i > 0 && core_env2

if разветвляется на МЕТКА 4 (если условие true) и МЕТКА 5 (если условие false)
// ============================================================================ МЕТКА 4
Input = n > 0 && s = s0 && core_env1 && OO && i > 0 && core_env2 && j >= 0 && s[j] > s[u]
core_env2 = A m (max(0, j+1) <= m <= i-1 --> s[m] <= s[u])

u <= j
j <= j - 1

Output = n > 0 && s = s0 && core_env1 && OO && i > 0 && core_env2

Верно, т.к. после выполнения операций
    output:core_env2 =
        = A m (max(0, j+1) <= m <= i-1 --> s[m] <= s[u]) =
        = A m (max(0, j+1+1) <= m <= i-1 --> s[m] <= s[u])                                && s[j+1] <= s[u] =
        = A m (max(0, j+1+1) <= m <= i-1 --> s[m] <= input:(s[u]) < input:(s[j]) = s[u]) && input:(s[j]) <= input:(s[j]) = true && true
// ============================================================================
=> TRUE

// ============================================================================ МЕТКА 5
Input = n > 0 && s = s0 && core_env1 && OO && i > 0 && core_env2 && j >= 0 && s[j] <= s[u]
core_env2 = A m (max(0, j+1) <= m <= i-1 --> s[m] <= s[u])

j <= j - 1

Output = n > 0 && s = s0 && core_env1 && OO && i > 0 && core_env2

Верно, т.к. после выполнения операций
    output:core_env2 =
        = A m (max(0, j+1) <= m <= i-1 --> s[m] <= s[u]) =
        = A m (max(0, j+1+1) <= m <= i-1 --> s[m] <= s[u]) && s[j+1] <= s[u] =
        = A m (max(0, j+1+1) <= m <= i-1 --> s[m] <= s[u]) && input:(s[j]) <= input:(s[u]) = true && true
// ============================================================================
=> TRUE

// ============================================================================ МЕТКА 2
Input = while_output = n > 0 && s = s0 && core_env1 && OO && i > 0 && A m (0 <= m <= i-1 --> s[m] <= s[u])
core_env1 = A d ( max(i, 0) < d <= n-1 --> A j, k ( 0 <= j <= d <= k <= n-1 --> s[j] <= s[k]))

y <= s[u]; s[u] <= s[i]; s[i] <= y;
i <= i - 1;

Output = n > 0 && s = s0 && core_env1 && OO

Действительно, т.к.
    output:core_env1 = 
        = A d ( max(i, 0) < d <= n-1 --> A j, k ( 0 <= j <= d <= k <= n-1 --> s[j] <= s[k])) =
        = A d ( max(i+1, 0) < d <= n-1 --> A j, k ( 0 <= j <= d <= k <= n-1 --> s[j] <= s[k])) &&
            && A j, k ( 0 <= j <= i <= k <= n-1 --> s[j] <= s[k]) =
        = input:core_env1 &&
            && A j, k ( 0 <= j <= input(i)-1 <= k <= n-1 --> s[j] <= s[k]) =
        = input:core_env1 &&
            && A j, k ( 0 <= j <= input(i)-1 <= k { k != input(i) } <= n-1 --> s[j] <= input(s[u]) = output(s[i]) <= s[k]) && тоже для k = input(i), но тогда s[k] = input(s[u]) =
        = true && true && true

    OO = true, т.к. "y <= s[u]; s[u] <= s[i]; s[i] <= y;" единственная строка изменяющая OO, и
    для некоторого x = s[u], одно из a' (и все возможные подмножества E j1, j2 ..., ja') убудет (если s[u] != s[i]), но тогда s[i] <= y - вернёт все эти комбинации => для всех наборов для которых выражение было верно, выражение так и останется верным
    усли же s[u] == s[i], то OO вообще не изменится
// ============================================================================
=> TRUE

// ============================================================================


Итак, мы доказали, что программа частично корректна, т.е. всегда когда она завершается - она корректна.

(* тотальная корректность верна, но можно было проще: а. внешний цикл останавливается, т.к. i опускается и не ниже ноля; б. для каждого i внутренний цикл останавливается, т.к. j опускается и не ниже ноля *)
Теперь докажем тотальную корректность, для этого докажем, что она всегда корректна:
Рассмотрим вектор длинной n со значениями = n
(n, n, n, ..., n)
Для каждого i и каждого j при уменьшении j на 1 уменьшаем i-й элемент на 1.
Заметим, что на каждом витке внутрненнего цикла обязательно происходит уменьшение, т.е. рано или поздно i-й элемент станет = 0, и мы выпадем из цикла, тогда во внешнем цикле неизбежно вычтется 1 из i и мы начнём уменьшать другую компоненту вектора n.

Итак, каждый виток внутреннего цикла неизбежно приводит к уменьшению одного из элементов вектора, причём уменьшение каждой компоненты не может быть больше, чем n, т.к. j <= i-1 и уменьшается <= n-1 и уменьшается => вектор нельзя уменьшить больше чем n*n раз => рано или поздно программа остановится, т.к. вектор невозможно уменьшить ниже (0, 0, 0, ... 0)

=> Программа тотально корректна.